FDL - Step of Proof: primrec

Step of Proof: primrec_add

11,40

Inference at * 2 1 1
Iof proof for Lemma primrec add:

1. T : Type
2. n :

3. 0 < n
4.

, b:T, c:({0..((n - 1)+m)

}

T).
4. primrec((n - 1)+m;b;c) = primrec(n - 1;primrec(m;b;c);

i,t. c(i+m,t))
5. m :

6. b : T
7. c : {0..(n+m)

}

T
8. b' : T
9. primrec(m;b;c) = b'
10. primrec((n - 1)+m;b;c) = primrec(n - 1;b';

i,t. c(i+m,t))

primrec(n+m;b;c) = primrec(n;b';

i,t. c(i+m,t))

by ((((RecUnfold `primrec` 0)

CollapseTHEN (Reduce 0))

)

CollapseTHEN (Repeat ((((

CSplitOnConclITE)

CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 1000:n

C)) (first_tok :t) inil_term)))

)

CollapseTHEN (Try (Complete (Auto_aux (first_nat 1:n

C) ((first_nat 2:n),(first_nat 3:n)) (first_tok SupInf:t) inil_term))))

))

C1: .....falsecase..... NILNIL

C1: 11.

(n+m = 0)

C1: 12.

(n = 0)

C1:

c(((n+m) - 1),primrec((n+m) - 1;b;c)) = c((n - 1)+m,primrec(n - 1;b';

i,t. c(i+m,t)))

Definitions ff, tt, P Q, if b then t else f fi , x:A. B(x), , t T, Y, primrec(n;b;c), P & Q, P Q, Unit, , ,

Lemmas not functionality wrt iff, assert of bnot, eqff to assert, assert of eq int, eqtt to assert, iff transitivity, not wf, bnot wf, assert wf, bool wf, eq int wf

Definitions	ff, tt, P Q, if b then t else f fi , x:A. B(x), , t T, Y, primrec(n;b;c), P & Q, P Q, Unit, , ,
Lemmas	not functionality wrt iff, assert of bnot, eqff to assert, assert of eq int, eqtt to assert, iff transitivity, not wf, bnot wf, assert wf, bool wf, eq int wf